Nuprl Lemma : ocmon_refl
13,42
postcript
pdf
g
:OCMon,
a
:|
g
|.
(
a
a
)
latex
Up
groups
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
AntiSym(
T
;
x
,
y
.
R
(
x
;
y
))
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
,
Order(
T
;
x
,
y
.
R
(
x
;
y
))
,
monot(
T
;
x
,
y
.
R
(
x
;
y
);
f
)
,
Cancel(
T
;
S
;
op
)
,
Linorder(
T
;
x
,
y
.
R
(
x
;
y
))
,
P
&
Q
Lemmas
ocmon
wf
,
ocmon
properties
origin
T, 
x:A. B(x), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), monot(T;x,y.R(x;y);f), Cancel(T;S;op), Linorder(T;x,y.R(x;y)), P & Q
(a 
a)